T:Type, f:(TT), R:(TT).
(x:T. R(x,x))
 (x, y, z:T. (x = f(y))  ((x = y))  y is f*(z)  R(y,z)  R(x,z))
 {x, y:T. x is f*(y)  R(x,y)} 

latex

Definitions	t  T, x:AB(x), Type, x:A. B(x), s = t, y is f*(x), , f(a), x(s1,s2), P  Q, , A, type List, A List, [car / cdr], y=f*(x) via L, <a, b>, Void, False, ||as||, #$n, a < b, i  j , hd(l), x:A  B(x), P & Q, A c B, {i..j}, , A  B, [], left + right, P  Q, Dec(P), b, x:A. B(x), b | a, a ~ b, a  b, a <p b, a < b, x f y, xL. P(x), (xL.P(x)), {T}, P  Q
Lemmas	fun-path-cons, decidable lt, hd wf, length wf1, not wf, int seg wf, fun-path wf, fun-connected wf